The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → a → Cons:Nil
Cons :: a → Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → a → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → a → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_7 :: Cons:Nil
hole_a2_7 :: a
hole_rev_l3_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_14_7 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil5_7 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_16_7 :: Nat → step_x_f:fleft_op_e_xs_1

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
step_x_f#1, foldr#3

(6) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → a → Cons:Nil
Cons :: a → Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → a → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → a → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_7 :: Cons:Nil
hole_a2_7 :: a
hole_rev_l3_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_14_7 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil5_7 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_16_7 :: Nat → step_x_f:fleft_op_e_xs_1

Generator Equations:
gen_Cons:Nil5_7(0) ⇔ Nil
gen_Cons:Nil5_7(+(x, 1)) ⇔ Cons(hole_a2_7, gen_Cons:Nil5_7(x))
gen_step_x_f:fleft_op_e_xs_16_7(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_16_7(+(x, 1)) ⇔ step_x_f(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(x))

The following defined symbols remain to be analysed:
step_x_f#1, foldr#3

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), gen_Cons:Nil5_7(b)) → gen_Cons:Nil5_7(+(+(1, n8_7), b)), rt ∈ Ω(1 + n8₇)

Induction Base:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(0), gen_Cons:Nil5_7(b)) →_R^Ω(1)
rev_l#2(gen_Cons:Nil5_7(b), hole_a2_7) →_R^Ω(1)
Cons(hole_a2_7, gen_Cons:Nil5_7(b))

Induction Step:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(+(n8_7, 1)), gen_Cons:Nil5_7(b)) →_R^Ω(1)
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), rev_l#2(gen_Cons:Nil5_7(b), hole_a2_7)) →_R^Ω(1)
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), Cons(hole_a2_7, gen_Cons:Nil5_7(b))) →_IH
gen_Cons:Nil5_7(+(+(1, +(b, 1)), c9_7))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → a → Cons:Nil
Cons :: a → Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → a → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → a → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_7 :: Cons:Nil
hole_a2_7 :: a
hole_rev_l3_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_14_7 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil5_7 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_16_7 :: Nat → step_x_f:fleft_op_e_xs_1

Lemmas:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), gen_Cons:Nil5_7(b)) → gen_Cons:Nil5_7(+(+(1, n8_7), b)), rt ∈ Ω(1 + n8₇)

Generator Equations:
gen_Cons:Nil5_7(0) ⇔ Nil
gen_Cons:Nil5_7(+(x, 1)) ⇔ Cons(hole_a2_7, gen_Cons:Nil5_7(x))
gen_step_x_f:fleft_op_e_xs_16_7(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_16_7(+(x, 1)) ⇔ step_x_f(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(x))

The following defined symbols remain to be analysed:
foldr#3

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
foldr#3(gen_Cons:Nil5_7(n528_7)) → gen_step_x_f:fleft_op_e_xs_16_7(n528_7), rt ∈ Ω(1 + n528₇)

Induction Base:
foldr#3(gen_Cons:Nil5_7(0)) →_R^Ω(1)
fleft_op_e_xs_1

Induction Step:
foldr#3(gen_Cons:Nil5_7(+(n528_7, 1))) →_R^Ω(1)
step_x_f(rev_l, hole_a2_7, foldr#3(gen_Cons:Nil5_7(n528_7))) →_IH
step_x_f(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(c529_7))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → a → Cons:Nil
Cons :: a → Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → a → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → a → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_7 :: Cons:Nil
hole_a2_7 :: a
hole_rev_l3_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_14_7 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil5_7 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_16_7 :: Nat → step_x_f:fleft_op_e_xs_1

Lemmas:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), gen_Cons:Nil5_7(b)) → gen_Cons:Nil5_7(+(+(1, n8_7), b)), rt ∈ Ω(1 + n8₇)
foldr#3(gen_Cons:Nil5_7(n528_7)) → gen_step_x_f:fleft_op_e_xs_16_7(n528_7), rt ∈ Ω(1 + n528₇)

Generator Equations:
gen_Cons:Nil5_7(0) ⇔ Nil
gen_Cons:Nil5_7(+(x, 1)) ⇔ Cons(hole_a2_7, gen_Cons:Nil5_7(x))
gen_step_x_f:fleft_op_e_xs_16_7(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_16_7(+(x, 1)) ⇔ step_x_f(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(x))

No more defined symbols left to analyse.

(13) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), gen_Cons:Nil5_7(b)) → gen_Cons:Nil5_7(+(+(1, n8_7), b)), rt ∈ Ω(1 + n8₇)

(14) BOUNDS(n^1, INF)

(15) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → a → Cons:Nil
Cons :: a → Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → a → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → a → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_7 :: Cons:Nil
hole_a2_7 :: a
hole_rev_l3_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_14_7 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil5_7 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_16_7 :: Nat → step_x_f:fleft_op_e_xs_1

Lemmas:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), gen_Cons:Nil5_7(b)) → gen_Cons:Nil5_7(+(+(1, n8_7), b)), rt ∈ Ω(1 + n8₇)
foldr#3(gen_Cons:Nil5_7(n528_7)) → gen_step_x_f:fleft_op_e_xs_16_7(n528_7), rt ∈ Ω(1 + n528₇)

Generator Equations:
gen_Cons:Nil5_7(0) ⇔ Nil
gen_Cons:Nil5_7(+(x, 1)) ⇔ Cons(hole_a2_7, gen_Cons:Nil5_7(x))
gen_step_x_f:fleft_op_e_xs_16_7(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_16_7(+(x, 1)) ⇔ step_x_f(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(x))

No more defined symbols left to analyse.

(16) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), gen_Cons:Nil5_7(b)) → gen_Cons:Nil5_7(+(+(1, n8_7), b)), rt ∈ Ω(1 + n8₇)

(17) BOUNDS(n^1, INF)

(18) Obligation:

Innermost TRS:
Rules:
rev_l#2(x8, x10) → Cons(x10, x8)
step_x_f#1(rev_l, x5, step_x_f(x2, x3, x4), x1) → step_x_f#1(x2, x3, x4, rev_l#2(x1, x5))
step_x_f#1(rev_l, x5, fleft_op_e_xs_1, x3) → rev_l#2(x3, x5)
foldr#3(Nil) → fleft_op_e_xs_1
foldr#3(Cons(x16, x6)) → step_x_f(rev_l, x16, foldr#3(x6))
main(Nil) → Nil
main(Cons(x8, x9)) → step_x_f#1(rev_l, x8, foldr#3(x9), Nil)

Types:
rev_l#2 :: Cons:Nil → a → Cons:Nil
Cons :: a → Cons:Nil → Cons:Nil
step_x_f#1 :: rev_l → a → step_x_f:fleft_op_e_xs_1 → Cons:Nil → Cons:Nil
rev_l :: rev_l
step_x_f :: rev_l → a → step_x_f:fleft_op_e_xs_1 → step_x_f:fleft_op_e_xs_1
fleft_op_e_xs_1 :: step_x_f:fleft_op_e_xs_1
foldr#3 :: Cons:Nil → step_x_f:fleft_op_e_xs_1
Nil :: Cons:Nil
main :: Cons:Nil → Cons:Nil
hole_Cons:Nil1_7 :: Cons:Nil
hole_a2_7 :: a
hole_rev_l3_7 :: rev_l
hole_step_x_f:fleft_op_e_xs_14_7 :: step_x_f:fleft_op_e_xs_1
gen_Cons:Nil5_7 :: Nat → Cons:Nil
gen_step_x_f:fleft_op_e_xs_16_7 :: Nat → step_x_f:fleft_op_e_xs_1

Lemmas:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), gen_Cons:Nil5_7(b)) → gen_Cons:Nil5_7(+(+(1, n8_7), b)), rt ∈ Ω(1 + n8₇)

Generator Equations:
gen_Cons:Nil5_7(0) ⇔ Nil
gen_Cons:Nil5_7(+(x, 1)) ⇔ Cons(hole_a2_7, gen_Cons:Nil5_7(x))
gen_step_x_f:fleft_op_e_xs_16_7(0) ⇔ fleft_op_e_xs_1
gen_step_x_f:fleft_op_e_xs_16_7(+(x, 1)) ⇔ step_x_f(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(x))

No more defined symbols left to analyse.

(19) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
step_x_f#1(rev_l, hole_a2_7, gen_step_x_f:fleft_op_e_xs_16_7(n8_7), gen_Cons:Nil5_7(b)) → gen_Cons:Nil5_7(+(+(1, n8_7), b)), rt ∈ Ω(1 + n8₇)

(20) BOUNDS(n^1, INF)